/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */

package chameleon.model.formula.parser;

/**
 * This class is a parser for an ltl formula which accepts : Next, Until,
 * always and eventually.
 */

import chameleon.model.formula.*;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.util.Stack;

/**
 * This class creates an LTL formula. The syntax is the following : 
 * 
 * f :: True | False | !f | X f | f && f | f U f | (f)
 *
 * The suported operator are :
 * !,X,F,G,<->,->,U,&&,||
 *
 *
 * @author simon
 */
public class LtlParser extends AbstractParser {

    public LtlParser () throws FileNotFoundException{
        super();
    }

    public LtlParser (String input) throws FileNotFoundException{
        super();
        lineRead = input.replaceAll("\\s", "");
    }

    private void initParser(String input){
        pos_ = 0;
        stackFormula_ = new Stack();
        stackOperator_ = new Stack();
        lineRead = input;
    }

    /**
     * Return the new token.
     *
     * @return
     * @throws IOException
     */

    @Override
    protected Word nextToken() {

        String prop ="";
        char[] line = lineRead.toCharArray();
        char charRead;
        boolean haveProp = false;
        boolean isInt = false;
        while (lineRead !=null ){

            if (pos_ == line.length){
                if (haveProp){
                    haveProp = false;
                    return returnToken(prop, isInt);
                }
                /*if((lineRead = br.readLine()) != null){
                    line = lineRead.toCharArray();
                    pos_ = 0;
                */
                else
                    return new Word (Tag.S_END,Tag.END);
            }

            charRead = line[pos_];
            pos_++;
            if (charRead == '~'){
                if (!haveProp)
                    return new Word (Tag.S_NOT,Tag.NOT);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            } 
            else if (charRead == 'X'){
                if (!haveProp)
                    return new Word(Tag.S_NEXT,Tag.NEXT);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == 'F'){
                if (!haveProp)
                    return new Word(Tag.S_EVENTUALLY,Tag.EVENTUALLY);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == 'G'){
                if (!haveProp)
                    return new Word(Tag.S_ALWAYS,Tag.ALWAYS);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == 'U'){
                if (!haveProp)
                    return new Word(Tag.S_UNTIL,Tag.UNTIL);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == '('){
                return new Word(Tag.S_OPEN_PARENTHESE,Tag.OPEN_PARENTHESE);
            }
            else if (charRead == ')'){
                if (!haveProp)
                    return new Word(Tag.S_CLOSE_PARENTHESE,Tag.CLOSE_PARENTHESE);
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == '&' && line[pos_] == '&'){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_AND, Tag.AND);
                }
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == '|' && line[pos_] == '|'){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_OR,Tag.OR);
                }
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == '-' && line[pos_] == '>'){
                if (!haveProp){
                    pos_++;
                    return new Word(Tag.S_IMPLIES,Tag.IMPLIES);
                }
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
            else if (charRead == '<' && line[pos_] == '-' && line[pos_+1] == '>'){
                if (!haveProp){
                    pos_ += 2;
                    return new Word(Tag.S_EQUIVALENCE,Tag.EQUIVALENCE);
                }
                else{
                    pos_--;
                    return returnToken(prop, isInt);
                }
            }
           /* else if (isLessThanMax(3) && ((charRead == 'T' && line[pos_] == 'r' && line[pos_+1] == 'u'
                    && line[pos_+2]=='e')
                    || (charRead == 't' && line[pos_] == 'r' && line[pos_+1] == 'u'
                    && line[pos_+2]=='e')
                    || (charRead == 'T' && line[pos_] == 'R' && line[pos_+1] == 'U'
                    && line[pos_+2]=='E'))){
                pos_ += 3;
                return new Word("True",Tag.TRUE);
            }
            else if (isLessThanMax(4) && ((charRead == 'F' && line[pos_] == 'a' && line[pos_+1] == 'l'
                    && line[pos_+2]=='s' && line[pos_+3] == 'e') 
                    ||(charRead == 'f' && line[pos_] == 'a' && line[pos_+1] == 'l'
                    && line[pos_+2]=='s' && line[pos_+3] == 'e') 
                    || (charRead == 'F' && line[pos_] == 'A' && line[pos_+1] == 'L'
                    && line[pos_+2]=='S' && line[pos_+3] == 'E') )){
                pos_ += 4;
                return new Word("False",Tag.FALSE);
            }
            else if (charRead >= '1' && charRead <= '9' && (isInt || !haveProp)){
                prop += charRead;
                isInt = true;
                haveProp = true;
            }*/
            /*else if (Character.isWhitespace(charRead)){
                if (haveProp)
                    return returnToken(prop, isInt);
            }
            /*else if (charRead == '\n'){
                lineRead = br.readLine();
            }*/
            else{
                //We have a proposition
                prop += charRead;
                haveProp = true;
            }
        }
        if (haveProp)
            return returnToken(prop, isInt);
        return new Word(Tag.S_END,Tag.END);
    }
    
    /**
     * This function determine if we have an interger or a proposition
     */
    
    private Word returnToken(String prop,boolean isInt){
        if (isInt)
            return new Word(prop, Tag.INTEGER);
        else
            return new Word(prop, Tag.PROPOSITION);
    }

    //START OF PARSING

     /**
     * The following methods are the description of the grammar.
     */

    public Formula createFormula(String formula) throws IOException{
        initParser(formula);
        return createFormula();
    }
    
    @Override
    public Formula createFormula() throws IOException{
        token_ = nextToken();
        FORMULA();
        if (!match(Tag.END))
            throw new RuntimeException("Ltl Parser :: semantic error");
        return (Formula) stackFormula_.pop();
    }

    @Override
    protected void FORMULA() throws IOException{
        bool();
        if (token_.getTag() != Tag.END)
            throw new RuntimeException("LTL parsing :: Semantic error");
    }
   
    
    
    private void factor() throws IOException{
        if (match(Tag.OPEN_PARENTHESE)){
            token_ = nextToken();
            bool();
            if (match(Tag.CLOSE_PARENTHESE))
                token_ = nextToken();
            else
                throw new RuntimeException("Ltl parsing ::  Missing closed parenthese");
        }
        else if (match(Tag.PROPOSITION) || match(Tag.TRUE) || match(Tag.FALSE) ||
                match (Tag.INTEGER)){
            BooleanParser parser = new BooleanParser(token_.toString());
            stackFormula_.push(parser.createFormula());
            token_ = nextToken();
        }
        else 
            ;
        //else
            //throw new RuntimeException("Ltl parsing :: semantic error");
    }
    
    private void createUnaryFormula(Operator op){
        stackFormula_.push(new Formula ((Formula)stackFormula_.pop(), op));
    }
    
    private void bool() throws IOException{
        EQ();
        //UNTIL();
    }

    private void EQ() throws IOException{
        IMPLIES();
        EQUIVALENCE();
    }

    private void EQUIVALENCE() throws IOException{
        if (match(Tag.EQUIVALENCE)){
            push(true);
            IMPLIES();
            EQUIVALENCE();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void IMPLIES() throws IOException{
        OR();
        IMPLIESP();
    }

    private void IMPLIESP() throws IOException{
        if (match(Tag.IMPLIES)){
            push(true);
            OR();
            IMPLIESP();
            createFormulaOnStack();
        }
    }

    private void OR() throws IOException {
        AND();
        ORP();
    }

    private void ORP() throws IOException{
        if (match(Tag.OR)){
            push(true);
            AND();
            ORP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }

    private void AND() throws IOException{
        UNTIL();
        ANDP();
    }

    private void ANDP() throws IOException {
        if (match(Tag.AND)){
            push(true);
            UNTIL();
            ANDP();
            createFormulaOnStack();
        }
        else
            ;//End of recursion
    }
    
    private void UNTIL() throws IOException{
        unary();
        UNTILP();
    }
    
    private void UNTILP() throws IOException{
        if (match(Tag.UNTIL)){
            push(true);
            unary();
            UNTIL();
            createFormulaOnStack();
        }
        else
            ;//END of recursion
    }
    
    
    private void unary() throws IOException{
        switch(token_.getTag()){
            case Tag.NOT:
                token_ = nextToken();
                unary();
                createUnaryFormula(new Operator(Tag.S_NOT));
                break;
            case Tag.NEXT:
                token_ = nextToken();
                unary();
                createUnaryFormula(new Operator(Tag.S_NEXT));
                break;
            case Tag.ALWAYS:
                token_ = nextToken();
                unary();
                createUnaryFormula(new Operator(Tag.S_ALWAYS));
                break;
            case Tag.EVENTUALLY:
                token_ = nextToken();
                unary();
                createUnaryFormula(new Operator(Tag.S_EVENTUALLY));
                break;
            default : 
                factor();
                break;
        }
    }
}
